$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop). \{!$x$:$T$ $\mid$ $P$($x$)\} $\in$ Type